w:World, e:E. FairFifo  (w-info(w;e)  ((:Id  Id) + (:(:IdLnk  E)  Id))) 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), kind(e), isrcv(k), left + right, P  Q, Dec(P), b, b, x:AB(x), x:A  B(x), P & Q, P  Q, Id, tag(k), sender(e), lnk(k), <a, b>, inr x , , s = t, , E, IdLnk, act(k), loc(e), inl x , islocal(k), Unit, kindcase(k; a.f(a); l,t.g(l;t) ), w-info(w;e), World, FairFifo
Lemmas	fair-fifo wf, world wf, eqtt to assert, iff transitivity, eqff to assert, islocal wf, w-loc wf, actof wf, IdLnk wf, w-E wf, bool wf, lnk wf, w-sender wf, tagof wf, Id wf, islocal-not-isrcv, not functionality wrt iff, assert of bnot, bnot wf, not wf, assert wf, decidable assert, isrcv wf, w-ekind wf